\begin{tabbing}
$\forall$$A$,$B$:Type.
\\[0ex]strong{-}subtype($A$; $B$)
\\[0ex]$\Rightarrow$ \=($\forall$$P$:($A$$\rightarrow$prop\{i:l\}), $Q$:($B$$\rightarrow$prop\{i:l\}).\+
\\[0ex]($\forall$$x$:$A$. $P$($x$) $\Rightarrow$ $Q$($x$)) $\Rightarrow$ strong{-}subtype(\{$x$:$A$$\mid$ $P$($x$)\} ; \{$x$:$B$$\mid$ $Q$($x$)\} ))
\-
\end{tabbing}